maname-deq()  EqDecider(MaName) 

latex

Definitions	IdDeq, t  T, Id, x:A. B(x), product-deq(A;B;a;b), locknd-deq(), x:A  B(x), LocKnd, union-deq(A;B;a;b), maname-deq(), MaName
Lemmas	union-deq wf, LocKnd wf, locknd-deq wf, product-deq wf, Id wf, id-deq wf